SherbyNet - /page/wikibook/entry.mu

Micron Document

<!DOCTYPE html>

<title>Communicating finite-state machine</title>

</head>

Communicating finite-state machine

</h1>

</header>

<div id="mw-content-text" class="mw-body-content mw-content-ltr" lang="en" dir="ltr"><div class="mw-content-ltr mw-parser-output" lang="en" dir="ltr">In <a href="Computer_science" title="Computer science">computer science</a>, a communicating finite-state machine is a <a href="Finite-state_machine" title="Finite-state machine">finite-state machine</a> labeled with "receive" and "send" operations over some alphabet of channels. They were introduced by Brand and Zafiropulo,<a href="#cite_note-Brand,_Zafiropulo-1">[1]</a> and can be used as a model of <a href="Concurrency_(computer_science)" title="Concurrency (computer science)">concurrent</a> processes like <a href="Petri_nets" class="mw-redirect" title="Petri nets">Petri nets</a>. Communicating finite-state machines are used frequently for modeling a communication protocol since they make it possible to detect major protocol design errors, including boundedness, deadlocks, and unspecified receptions.<a href="#cite_note-Rosier,_Gouda-2">[2]</a>

The advantage of communicating finite-state machines is that they make it possible to decide many properties in communication protocols, beyond the level of just detecting such properties. This advantage rules out the need for human assistance or restriction in generality.<a href="#cite_note-Brand,_Zafiropulo-1">[1]</a>

Communicating finite-state machines can be more powerful than finite-state machines in situations where the propagation delay is not negligible (so that several messages can be in transit at one time) and in situations where it is natural to describe the protocol parties and the communication medium as separate entities.<a href="#cite_note-Brand,_Zafiropulo-1">[1]</a>

<div class="mw-heading mw-heading2"><h2 id="Communicating_hierarchical_state_machine">Communicating hierarchical state machine</h2></div>

Hierarchical state machines are finite-state machines whose states themselves can be other machines. Since a communicating finite-state machine is characterized by concurrency, the most notable trait in a communicating hierarchical state machine is the coexistence of hierarchy and concurrency. This has been considered highly suitable as it signifies stronger interaction inside the machine.

However, it was proved that the coexistence of hierarchy and concurrency intrinsically costs language inclusion, language equivalence, and all of universality.<a href="#cite_note-3">[3]</a>

<div class="mw-heading mw-heading2"><h2 id="Definition">Definition</h2></div>

<div class="mw-heading mw-heading3"><h3 id="Protocol">Protocol</h3></div>

For an arbitrary positive integer <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle N}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle N}</annotation>

</semantics>

</math><img src="./f5e3890c981ae85503089652feb48b191b57aae3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.064ex; height:2.176ex;" alt="{\displaystyle N}" loading="lazy">, a protocol <a href="#cite_note-Brand,_Zafiropulo-1">[1]</a>: 3 with <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle N}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle N}</annotation>

</semantics>

</math><img src="./f5e3890c981ae85503089652feb48b191b57aae3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.064ex; height:2.176ex;" alt="{\displaystyle N}" loading="lazy"> process(es) is a quadruple <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \{(S_{i})_{i=1}^{N},\ (o_{i})_{i=1}^{N},\ (M_{i,j})_{i,j=1}^{N},\ ({\mathtt {succ}})_{i=1}^{N}\}}">

<msub>

</mrow>

</msub>

</mrow>

</mrow>

</msubsup>

<msub>

</mrow>

</msub>

</mrow>

</mrow>

</msubsup>

<msub>

</mrow>

</msub>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \{(S_{i})_{i=1}^{N},\ (o_{i})_{i=1}^{N},\ (M_{i,j})_{i,j=1}^{N},\ ({\mathtt {succ}})_{i=1}^{N}\}}</annotation>

</semantics>

</math><img src="./ed9a538aa64a53c47e58348171c6c7f29fe6d287.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.338ex; width:40.364ex; height:3.509ex;" alt="{\displaystyle \{(S_{i})_{i=1}^{N},\ (o_{i})_{i=1}^{N},\ (M_{i,j})_{i,j=1}^{N},\ ({\mathtt {succ}})_{i=1}^{N}\}}" loading="lazy"> with:

<msub>

</mrow>

</msub>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (S_{i})_{i=1}^{N}}</annotation>

</semantics>

</math><img src="./eac4ac2b0320fed149fa8ae05a4efcfd2c6159d8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:6.934ex; height:3.176ex;" alt="{\displaystyle (S_{i})_{i=1}^{N}}" loading="lazy">, a sequence of <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle N}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle N}</annotation>

</semantics>

</math><img src="./f5e3890c981ae85503089652feb48b191b57aae3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.064ex; height:2.176ex;" alt="{\displaystyle N}" loading="lazy"> disjoint finite sets. Each set is used to represent a process, and each element of <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S_{i}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle S_{i}}</annotation>

</semantics>

</math><img src="./de6e810a93f67802ecb603ee0e3324005c6e583e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.225ex; height:2.509ex;" alt="{\displaystyle S_{i}}" loading="lazy"> represents a possible state of the <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle i}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle i}</annotation>

</semantics>

<msub>

</mrow>

</msub>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (o_{i})_{i=1}^{N}}</annotation>

</semantics>

</math><img src="./d129bf6d50bac2ba548e6d98340c78d8cf40725f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:6.637ex; height:3.176ex;" alt="{\displaystyle (o_{i})_{i=1}^{N}}" loading="lazy"> (with <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle o_{i}\in S_{i}}">

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle o_{i}\in S_{i}}</annotation>

</semantics>

</math><img src="./515d754e01a01cd81bd21dd3fd3611f92a5d87a5.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:6.993ex; height:2.509ex;" alt="{\displaystyle o_{i}\in S_{i}}" loading="lazy">), a sequence representing the initial state of each process.</li>

<msub>

</mrow>

</msub>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (M_{i,j})_{i,j=1}^{N}}</annotation>

</semantics>

</math><img src="./f7c756b3c878051d1ba5fb3751b4227a85955133.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.338ex; width:10.033ex; height:3.509ex;" alt="{\displaystyle (M_{i,j})_{i,j=1}^{N}}" loading="lazy">, a finite sequence of <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle N^{2}}">

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle N^{2}}</annotation>

</semantics>

</math><img src="./fe131b76af8a2bc86e01b14a7ba843db69c1a164.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:3.177ex; height:2.676ex;" alt="{\displaystyle N^{2}}" loading="lazy"> disjoint finite sets such that each set <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle M_{i,j}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle M_{i,j}}</annotation>

</semantics>

</math><img src="./0471da86bad57963868302a83a9decf6804d4197.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:4.189ex; height:2.843ex;" alt="{\displaystyle M_{i,j}}" loading="lazy"> represents the possible messages which may be sent from process <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle i}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle i}</annotation>

</semantics>

</math><img src="./add78d8608ad86e54951b8c8bd6c8d8416533d20.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.802ex; height:2.176ex;" alt="{\displaystyle i}" loading="lazy"> to process <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle j}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle j}</annotation>

</semantics>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle i=j}</annotation>

</semantics>

</math><img src="./706e0928b2bf0f24076b0c90bb20616ff2068343.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.859ex; height:2.509ex;" alt="{\displaystyle i=j}" loading="lazy">, then <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle M_{i,j}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle M_{i,j}}</annotation>

</semantics>

</mrow>

</mrow>

</mrow>

</msubsup>

<msub>

</mrow>

</msub>

</mrow>

</mrow>

</munderover>

<mrow>

<mrow>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle ({\mathtt {succ}})_{i=1}^{N}:S_{i}\times \bigcup _{j=1}^{N}\left(M_{j,i}^{[+]}\cup M_{i,j}^{[-]}\right)\mapsto S_{i}}</annotation>

</semantics>

</math><img src="./b034c1ca32962aade65f1640d63503ab13265121.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -3.338ex; width:40.804ex; height:7.676ex;" alt="{\displaystyle ({\mathtt {succ}})_{i=1}^{N}:S_{i}\times \bigcup _{j=1}^{N}\left(M_{j,i}^{[+]}\cup M_{i,j}^{[-]}\right)\mapsto S_{i}}" loading="lazy"> is a sequence of transition functions. Each function modelizes the transition which can be taken by emitting or receiving any message. With respect to process <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle i}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle i}</annotation>

</semantics>

</math><img src="./add78d8608ad86e54951b8c8bd6c8d8416533d20.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.802ex; height:2.176ex;" alt="{\displaystyle i}" loading="lazy">, the symbol <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle [+]}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle [+]}</annotation>

</semantics>

</math><img src="./b0583e317cc78da9cf49aa02cd71fa5e6ab6e27c.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:3.102ex; height:2.843ex;" alt="{\displaystyle [+]}" loading="lazy"> is used to note a message that can be received and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle [-]}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle [-]}</annotation>

</semantics>

</math><img src="./25fa02b41c948a16ec1010ba03c183ef6a16f44c.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:3.102ex; height:2.843ex;" alt="{\displaystyle [-]}" loading="lazy"> a message that can be sent.</li></ul>

<div class="mw-heading mw-heading3"><h3 id="Global_state">Global state</h3></div>

A global state is a pair <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \langle S,C\rangle }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \langle S,C\rangle }</annotation>

</semantics>

</math><img src="./893a2107fbe6feb1ef45194194c5f5f9dfd9bcb9.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:6.109ex; height:2.843ex;" alt="{\displaystyle \langle S,C\rangle }" loading="lazy"> where

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle S=(s_{1},...,s_{N})}</annotation>

</semantics>

</math><img src="./c4caa376dcfc05163581532ef34f7a53c230e20a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:16.503ex; height:2.843ex;" alt="{\displaystyle S=(s_{1},...,s_{N})}" loading="lazy"> is an ordered collection of states such that each <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle s_{i}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle s_{i}}</annotation>

</semantics>

</math><img src="./cfda82668232cbdc0874ed28ab8b6079420d1ffe.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.89ex; height:2.009ex;" alt="{\displaystyle s_{i}}" loading="lazy"> represents a state of the <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle i}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle i}</annotation>

</semantics>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle C}</annotation>

</semantics>

</math><img src="./4fc55753007cd3c18576f7933f6f089196732029.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.766ex; height:2.176ex;" alt="{\displaystyle C}" loading="lazy"> is an <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle N\times N}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle N\times N}</annotation>

</semantics>

</math><img src="./99a86c5231bb3cbb863d9d428ebe9ac8db8d4ffb.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:6.968ex; height:2.176ex;" alt="{\displaystyle N\times N}" loading="lazy"> matrix such that each <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle c_{i,j}\in C}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle c_{i,j}\in C}</annotation>

</semantics>

</math><img src="./8a88c178af0d6555c4f99fb1f1a095647cd58380.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:7.548ex; height:2.843ex;" alt="{\displaystyle c_{i,j}\in C}" loading="lazy"> is a subsequence of <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle M_{i,j}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle M_{i,j}}</annotation>

</semantics>

The initial global state is a pair <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \langle O,\mathrm {E} \rangle }">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \langle O,\mathrm {E} \rangle }</annotation>

</semantics>

</math><img src="./56a9973b8f9b93c4769260f5bb293ee9444a95b7.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:6.199ex; height:2.843ex;" alt="{\displaystyle \langle O,\mathrm {E} \rangle }" loading="lazy"> where

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle O=(o_{1},...,o_{N})}</annotation>

</semantics>

</math><img src="./d0a7a4de7553bb7dad8de475a593d0aba1022ad8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:16.852ex; height:2.843ex;" alt="{\displaystyle O=(o_{1},...,o_{N})}" loading="lazy"></li>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \mathrm {E} }</annotation>

</semantics>

</math><img src="./be1811407dea8b43727d28dbe8da7251985b03e8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.583ex; height:2.176ex;" alt="{\displaystyle \mathrm {E} }" loading="lazy"> is defined to be an <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle N\times N}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle N\times N}</annotation>

</semantics>

</math><img src="./99a86c5231bb3cbb863d9d428ebe9ac8db8d4ffb.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:6.968ex; height:2.176ex;" alt="{\displaystyle N\times N}" loading="lazy"> matrix such that for all <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle i,j\in \{1,...,N\}}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle i,j\in \{1,...,N\}}</annotation>

</semantics>

</math><img src="./22c6cbbe44f9d83e13653bcd2ed55b72e7c15db2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:16.356ex; height:2.843ex;" alt="{\displaystyle i,j\in \{1,...,N\}}" loading="lazy">, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle E_{i,j}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle E_{i,j}}</annotation>

</semantics>

</math><img src="./e7814421833a1b6fae2769bb795158a0c02ecda0.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:3.65ex; height:2.843ex;" alt="{\displaystyle E_{i,j}}" loading="lazy"> equals the empty word, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \epsilon }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \epsilon }</annotation>

</semantics>

</math><img src="./c3837cad72483d97bcdde49c85d3b7b859fb3fd2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.944ex; height:1.676ex;" alt="{\displaystyle \epsilon }" loading="lazy">.</li></ul>

There are two kinds of steps, steps in which message are received and steps in which messages are sent.

A step in which the <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle j}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle j}</annotation>

</semantics>

previously sent by the <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle i}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle i}</annotation>

</semantics>

<mrow>

<mrow>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<mrow>

<mtr>

<mtd>

<msub>

</mrow>

</msub>

</mtd>

<mtd>

</mtd>

<mtd>

<msub>

</mrow>

</msub>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

<msub>

</mrow>

</msub>

</mtd>

<mtd>

</mtd>

<mtd>

<msub>

</mrow>

</msub>

</mtd>

</mtr>

</mtable>

</mrow>

</mrow>

</mrow>

<mrow>

<mrow>

<msub>

</mrow>

</msub>

</mrow>

</msubsup>

<msub>

</mrow>

</msub>

<mrow>

<mtr>

<mtd>

<msub>

</mrow>

</msub>

</mtd>

<mtd>

</mtd>

<mtd>

<msub>

</mrow>

</msub>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

<msub>

</mrow>

</msub>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

<msub>

</mrow>

</msub>

</mtd>

<mtd>

</mtd>

<mtd>

<msub>

</mrow>

</msub>

</mtd>

</mtr>

</mtable>

</mrow>

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \left\langle (s_{1},\dots ,s_{j},\dots ,s_{n}),\left({\begin{array}{lll}c_{1,1}&\dots &c_{1,n}\\\dots &\dots &\dots \\\dots &m_{i,j}c_{i,j}&\dots \\\dots &\dots &\dots \\c_{n,1}&\dots &c_{n,n}\end{array}}\right)\right\rangle \vdash \left\langle (s_{1},\dots ,s'_{j},\dots ,s_{n}),\left({\begin{array}{lll}c_{1,1}&\dots &c_{1,n}\\\dots &\dots &\dots \\\dots &c_{i,j}&\dots \\\dots &\dots &\dots \\c_{n,1}&\dots &c_{n,n}\end{array}}\right)\right\rangle }</annotation>

</semantics>

</math><img src="./21a97427984fdff17671e21947c21f195404ef14.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -7.671ex; width:92.642ex; height:16.509ex;" alt="{\displaystyle \left\langle (s_{1},\dots ,s_{j},\dots ,s_{n}),\left({\begin{array}{lll}c_{1,1}&\dots &c_{1,n}\\\dots &\dots &\dots \\\dots &m_{i,j}c_{i,j}&\dots \\\dots &\dots &\dots \\c_{n,1}&\dots &c_{n,n}\end{array}}\right)\right\rangle \vdash \left\langle (s_{1},\dots ,s'_{j},\dots ,s_{n}),\left({\begin{array}{lll}c_{1,1}&\dots &c_{1,n}\\\dots &\dots &\dots \\\dots &c_{i,j}&\dots \\\dots &\dots &\dots \\c_{n,1}&\dots &c_{n,n}\end{array}}\right)\right\rangle }" loading="lazy"> when <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathtt {succ}}_{i}(s_{j},+m_{i,j})=s'_{j}}">

<msub>

</mrow>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\mathtt {succ}}_{i}(s_{j},+m_{i,j})=s'_{j}}</annotation>

</semantics>

</math><img src="./1bf805d2d474f9d2117ae8e07c4668a50f0da2fe.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.338ex; width:21.407ex; height:3.343ex;" alt="{\displaystyle {\mathtt {succ}}_{i}(s_{j},+m_{i,j})=s'_{j}}" loading="lazy">, with <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle m'_{i,j}\in M_{i,j}}">

</mrow>

</msubsup>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle m'_{i,j}\in M_{i,j}}</annotation>

</semantics>

</math><img src="./15eae730901bb6aa5d93b20ddaaaccd6b2c855b1.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.338ex; width:11.004ex; height:3.176ex;" alt="{\displaystyle m'_{i,j}\in M_{i,j}}" loading="lazy">. Similarly, a pair in which a message is sent by the <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle i}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle i}</annotation>

</semantics>

</math><img src="./add78d8608ad86e54951b8c8bd6c8d8416533d20.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.802ex; height:2.176ex;" alt="{\displaystyle i}" loading="lazy">-th process to the <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle j}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle j}</annotation>

</semantics>

</math><img src="./2f461e54f5c093e92a55547b9764291390f0b5d0.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.027ex; width:0.985ex; height:2.509ex;" alt="{\displaystyle j}" loading="lazy">-th one is a pair of the form <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \left\langle (s_{1},\dots ,s_{i},\dots ,s_{n}),\left({\begin{array}{lll}c_{1,1}&\dots &c_{1,n}\\\dots &\dots &\dots \\\dots &c_{i,j}&\dots \\\dots &\dots &\dots \\c_{n,1}&\dots &c_{n,n}\end{array}}\right)\right\rangle \vdash \left\langle (s_{1},\dots ,s'_{i},\dots ,s_{n}),\left({\begin{array}{lll}c_{1,1}&\dots &c_{1,n}\\\dots &\dots &\dots \\\dots &m_{i,j}c_{i,j}&\dots \\\dots &\dots &\dots \\c_{n,1}&\dots &c_{n,n}\end{array}}\right)\right\rangle }">

<mrow>

<mrow>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<mrow>

<mtr>

<mtd>

<msub>

</mrow>

</msub>

</mtd>

<mtd>

</mtd>

<mtd>

<msub>

</mrow>

</msub>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

<msub>

</mrow>

</msub>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

<msub>

</mrow>

</msub>

</mtd>

<mtd>

</mtd>

<mtd>

<msub>

</mrow>

</msub>

</mtd>

</mtr>

</mtable>

</mrow>

</mrow>

</mrow>

<mrow>

<mrow>

<msub>

</mrow>

</msub>

</mrow>

</msubsup>

<msub>

</mrow>

</msub>

<mrow>

<mtr>

<mtd>

<msub>

</mrow>

</msub>

</mtd>

<mtd>

</mtd>

<mtd>

<msub>

</mrow>

</msub>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

<msub>

</mrow>

</msub>

</mtd>

<mtd>

</mtd>

<mtd>

<msub>

</mrow>

</msub>

</mtd>

</mtr>

</mtable>

</mrow>

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \left\langle (s_{1},\dots ,s_{i},\dots ,s_{n}),\left({\begin{array}{lll}c_{1,1}&\dots &c_{1,n}\\\dots &\dots &\dots \\\dots &c_{i,j}&\dots \\\dots &\dots &\dots \\c_{n,1}&\dots &c_{n,n}\end{array}}\right)\right\rangle \vdash \left\langle (s_{1},\dots ,s'_{i},\dots ,s_{n}),\left({\begin{array}{lll}c_{1,1}&\dots &c_{1,n}\\\dots &\dots &\dots \\\dots &m_{i,j}c_{i,j}&\dots \\\dots &\dots &\dots \\c_{n,1}&\dots &c_{n,n}\end{array}}\right)\right\rangle }</annotation>

</semantics>

</math><img src="./334896dbff4e5ec1864a7e15e51a5eb3a15707a4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -7.671ex; width:92.422ex; height:16.509ex;" alt="{\displaystyle \left\langle (s_{1},\dots ,s_{i},\dots ,s_{n}),\left({\begin{array}{lll}c_{1,1}&\dots &c_{1,n}\\\dots &\dots &\dots \\\dots &c_{i,j}&\dots \\\dots &\dots &\dots \\c_{n,1}&\dots &c_{n,n}\end{array}}\right)\right\rangle \vdash \left\langle (s_{1},\dots ,s'_{i},\dots ,s_{n}),\left({\begin{array}{lll}c_{1,1}&\dots &c_{1,n}\\\dots &\dots &\dots \\\dots &m_{i,j}c_{i,j}&\dots \\\dots &\dots &\dots \\c_{n,1}&\dots &c_{n,n}\end{array}}\right)\right\rangle }" loading="lazy"> when <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathtt {succ}}_{i}(s_{i},-m_{i,j})=s'_{i}}">

<msub>

</mrow>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\mathtt {succ}}_{i}(s_{i},-m_{i,j})=s'_{i}}</annotation>

</semantics>

</math><img src="./143cd2ffb195ba5eea4e541897800bf22abd3ad3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:21.187ex; height:3.009ex;" alt="{\displaystyle {\mathtt {succ}}_{i}(s_{i},-m_{i,j})=s'_{i}}" loading="lazy">

A run is a sequence of global states such that a step relate a state to the next one, and such that the first state is initial.

It is said that a global state <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \langle S,C\rangle }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \langle S,C\rangle }</annotation>

</semantics>

<div class="mw-heading mw-heading3"><h3 id="Problems">Problems</h3></div>

It has been proved with the introduction of the concept itself that when two finite-state machines communicate with only one type of messages, boundedness, deadlocks, and unspecified reception state can be decided and identified while such is not the case when the machines communicate with two or more types of messages. Later, it has been further proved that when only one finite-state machine communicates with single type of message while the communication of its partner is unconstrained, we can still decide and identify boundedness, deadlocks, and unspecified reception state.<a href="#cite_note-Rosier,_Gouda-2">[2]</a>

It has been further proved that when the message priority relation is empty, boundedness, deadlocks and unspecified reception state can be decided even under the condition in which there are two or more types of messages in the communication between finite-state machines.<a href="#cite_note-4">[4]</a>

Boundedness, deadlocks, and unspecified reception state are all decidable in polynomial time (which means that a particular problem can be solved in tractable, not infinite, amount of time) since the decision problems regarding them are nondeterministic logspace complete.<a href="#cite_note-Rosier,_Gouda-2">[2]</a>

<div class="mw-heading mw-heading2"><h2 id="Extensions">Extensions</h2></div>

Some extensions considered are:

<ul><li>having a notation to state that some states may not receive any message,</li>

<li>messages are received in different orders, such as FILO,</li>

<li>some messages may get lost,</li></ul>

<div class="mw-heading mw-heading3"><h3 id="Channel_system">Channel system</h3></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .hatnote{font-style:italic}.mw-parser-output div.hatnote{padding-left:1.6em;margin-bottom:0.5em}.mw-parser-output .hatnote i{font-style:normal}.mw-parser-output .hatnote+link+.hatnote{margin-top:-0.5em}@media print{body.ns-0 .mw-parser-output .hatnote{display:none!important}}

/* end https://en.wikipedia.org/ */

</style><div role="note" class="hatnote navigation-not-searchable">Main article: <a href="Channel_system_(computer_science)" title="Channel system (computer science)">Channel system (computer science)</a></div>

A channel system is essentially a version of communicating finite-state machine in which the machine is not divided into distinct process. Thus, there is a single state of state, and there is no restriction relating which system can read/write on any channel.

Formally, given a protocol <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \langle (S_{i})_{i=1}^{n},(o_{i})_{i=1}^{n},(M_{i,j})_{i,j=1}^{n},({\mathtt {succ}})_{i}\rangle }">

<msub>

</mrow>

</msub>

</mrow>

</mrow>

</msubsup>

<msub>

</mrow>

</msub>

</mrow>

</mrow>

</msubsup>

<msub>

</mrow>

</msub>

</mrow>

</mrow>

</msubsup>

</mrow>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \langle (S_{i})_{i=1}^{n},(o_{i})_{i=1}^{n},(M_{i,j})_{i,j=1}^{n},({\mathtt {succ}})_{i}\rangle }</annotation>

</semantics>

</math><img src="./123719c87011cb1483c029ad3118538768c7bae6.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.338ex; width:36.006ex; height:3.343ex;" alt="{\displaystyle \langle (S_{i})_{i=1}^{n},(o_{i})_{i=1}^{n},(M_{i,j})_{i,j=1}^{n},({\mathtt {succ}})_{i}\rangle }" loading="lazy">, its associated channel system is <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \langle \prod (S_{i})_{i=1}^{n},(o_{i})_{i=1}^{n},\bigcup _{i,j=1}^{n}(M_{i,j}),\Delta \rangle }">

<msub>

</mrow>

</msub>

</mrow>

</mrow>

</msubsup>

<msub>

</mrow>

</msub>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</munderover>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \langle \prod (S_{i})_{i=1}^{n},(o_{i})_{i=1}^{n},\bigcup _{i,j=1}^{n}(M_{i,j}),\Delta \rangle }</annotation>

</semantics>

</math><img src="./3ff3bbd5f5f6ce742975c6e18b3c79940ef3e7fd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -3.338ex; width:33.188ex; height:7.176ex;" alt="{\displaystyle \langle \prod (S_{i})_{i=1}^{n},(o_{i})_{i=1}^{n},\bigcup _{i,j=1}^{n}(M_{i,j}),\Delta \rangle }" loading="lazy">, where <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Delta }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \Delta }</annotation>

</semantics>

</math><img src="./32769037c408874e1890f77554c65f39c523ebe2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.936ex; height:2.176ex;" alt="{\displaystyle \Delta }" loading="lazy"> is the set of <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle ((s_{1},\dots ,s_{j},\dots ,s_{n}),?m_{i,j},(s_{1},\dots ,{\mathtt {succ}}_{j}(s_{j},+m_{i,j}),\dots ,s_{n})}">

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle ((s_{1},\dots ,s_{j},\dots ,s_{n}),?m_{i,j},(s_{1},\dots ,{\mathtt {succ}}_{j}(s_{j},+m_{i,j}),\dots ,s_{n})}</annotation>

</semantics>

</math><img src="./adf614766d955bc23b5eb656507c8473f75b6093.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:59.702ex; height:3.009ex;" alt="{\displaystyle ((s_{1},\dots ,s_{j},\dots ,s_{n}),?m_{i,j},(s_{1},\dots ,{\mathtt {succ}}_{j}(s_{j},+m_{i,j}),\dots ,s_{n})}" loading="lazy"> and of <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle ((s_{1},\dots ,s_{i},\dots ,s_{n}),!m_{i,j},(s_{1},\dots ,{\mathtt {succ}}_{i}(s_{i},-m_{i,j}),\dots ,s_{n})}">

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle ((s_{1},\dots ,s_{i},\dots ,s_{n}),!m_{i,j},(s_{1},\dots ,{\mathtt {succ}}_{i}(s_{i},-m_{i,j}),\dots ,s_{n})}</annotation>

</semantics>

</math><img src="./89a70c972fddff3c1179539f203a6d12a0be6cd8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:58.921ex; height:3.009ex;" alt="{\displaystyle ((s_{1},\dots ,s_{i},\dots ,s_{n}),!m_{i,j},(s_{1},\dots ,{\mathtt {succ}}_{i}(s_{i},-m_{i,j}),\dots ,s_{n})}" loading="lazy">.

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

<li id="cite_note-Brand,_Zafiropulo-1">^ <a href="#cite_ref-Brand,_Zafiropulo_1-0">a</a> <a href="#cite_ref-Brand,_Zafiropulo_1-1">b</a> <a href="#cite_ref-Brand,_Zafiropulo_1-2">c</a> <a href="#cite_ref-Brand,_Zafiropulo_1-3">d</a> D. Brand and P. Zafiropulo. On communicating finite-state machines. Journal of the ACM, 30(2):323–342, 1983.

</li>

<li id="cite_note-Rosier,_Gouda-2">^ <a href="#cite_ref-Rosier,_Gouda_2-0">a</a> <a href="#cite_ref-Rosier,_Gouda_2-1">b</a> <a href="#cite_ref-Rosier,_Gouda_2-2">c</a> Rosier, Louis E; Gouda, Mohamed G. Deciding Progress for a Class of Communicating Finite State Machines. Austin: University of Texas at Austin, 1983.

</li>

<li id="cite_note-3"><a href="#cite_ref-3">^</a> Alur, Rajeev; Kannan, Sampath; Yannakakis, Mihalis. "Communicating hierarchical state machines," Automata, Languages and Programming. Prague: ICALP, 1999

</li>

<li id="cite_note-4"><a href="#cite_ref-4">^</a> Gouda, Mohamed G; Rosier, Louis E. "Communicating finite state machines with priority channels," Automata, Languages and Programming. Antwerp: ICALP, 1984

</li>

</ol></div></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2024-12-26" href="https://en.wikipedia.org/wiki/?title=Communicating_finite-state_machine&oldid=1265273115">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>